| Definitions | P   Q,  x:A. B(x), prop{i:l}, t  T,   x. t(x), event-info(ds;da), ma-valtype(da; k), es-hist{i:l}(es;e1;e2), top, P  Q, P  Q, P Q,  x:A. B(x), A c B, guard(T), sq_type(T), l_all(L; T; x.P(x)),  A, False, Y, map(f; as), subtype(S; T), i <z j,  b, i  z j, nth_tl(n;as), hd(l), ||as||, l[i], if b then t else f fi , ff, tt, null(as), last(L),  b, append(as; bs), True,  T, e[e1,e2).P(e), P  Q, e[e1,e2].P(e), es-le(es; e; e'), ecl-halt(ds; da; x), A B,  , e(e1,e2].P(e), (x l), x,y. t(x;y), star-append(T; P; Q), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), ecl-es-halt(es; x), lelt(i; j; k), int_seg(i; j), reduce(f; k; as), (i = j), upto(n), concat(ll), suptype(S; T), l_exists(L; T; x.P(x)), x(s), e2 = first e  e1.P(e), decidable(P), t.2, t.1, es-info(es;e), es-locl(es; e; e'), spreadn(a; x,y,z.t(x;y;z)), Unit,  , e[e1,e2].P(e), x(s1,s2),  , trans(T; x,y.E(x;y)),  |
| Lemmas | es-loc wf, es-hist wf, ecl-es-halt wf, iff wf, top wf, Kind-deq wf, fpf-cap wf, last lemma, null-es-hist, es-locl wf, null wf3, assert wf, not functionality wrt iff, es-interval wf, es-E wf, map wf, es-le-not-locl, l member wf, not wf, l all wf2, append wf, event-info wf, Knd sq, es-vartype wf, es-state-subtype, nil member, decidable false, length wf1, decidable es-le, decidable es-locl, es-interval-is-nil, non neg length, length-append, false wf, last append, pi1 wf, pi2 wf, last-es-hist, bool wf, true wf, squash wf, es-le wf, es-info wf, es-loc-pred, es-le-loc, es-locl-iff, es-pred wf, member-es-hist, es-le-pred, es-le weakening eq, es-locl transitivity1, es-hist-partition, general-append-cancellation, nat wf, length wf nat, es-interval-eq, es-val wf, Id wf, es-state-when wf, es-kind wf, le wf, ecl-halt wf, assert of bnot, eqff to assert, bnot wf, assert of eq int, eqtt to assert, iff transitivity, bool sq, eq int wf, bool cases, es-hist-is-append, ecl-halt-nil, iseg wf, decl-state wf, es-hist-iseg, es-le-iff, ecl-halt-ex, alle-between2 wf, assert of lt int, bnot of le int, lt int wf, alle-between1 wf, assert of le int, le int wf, select wf, l-all-iff, nat plus wf, nat plus inc, ecl-ex wf, iseg-es-hist, existse-between2 wf, eclrepeat wf, id-deq wf, ma-valtype wf, es-valtype wf, star-append wf, es-pstar-q wf, ifthenelse wf, upto wf, int seg wf, es-first wf, member map, decidable int equal, nat plus properties, es-le-trans, concat append, map append sq, concat wf, append assoc sq, append-nil, decidable assert, assert of null, es-hist-is-concat, Id sq, select member, eclact wf, subtype rel wf, eclthrow wf, eclcatch wf, l exists wf |
